3.1.1 Language Reference

3.1.1 Language Reference

The input language of CSP Module CSP# is mainly influenced by the classic Communicating Sequential Processes (CSP [Hoare85]). Nonetheless, we extend CSP with various useful language features to reach our goal. Examples include shared variables, arrays, asynchronous message passing channels and event annotations which capture a variety of fairness constraints.

Our modeling language is designed for automated system analysis. There are two other popular modeling languages working for the same purpose, namely machine readable CSP (which we will refer to as CSP_M) supported by the refinement checker FDR [AWR97] and Promela which is supported by the model checker SPIN [GJH97].

Compared to CSP_M, CSP# supports additional language features like shared variables, asynchronous communication channels and event associated programs, which offers users great flexibility in modeling. Furthermore, we give an interpretation of state/event Linear Temporal Logic in CSP# semantics framework, which allows temporal logic based model checking of CSP# models.
Compared to Promela, CSP# supports more process constructs, i.e., Promela is based on a subset of CSP, whereas all CSP models are valid CSP# models. In particular, CSP# inherits the classic trace, stable failures and failures/divergence semantics from CSP, and therefore, allows us to perform a variety of refinement checking. CSP# is also remotely related to other languages which are designed for model checking.

The language constructs of CSP# may be categorized into the following groups.

The first group is the core subset of CSP operators, including event-prefixing, internal/external choices, alphabetized lock-step synchronization, conditional branching, interrupt, recursion, etc.
The second group includes those language constructs which can be regarded as "syntactic sugar" (to CSP), including global shared variables, and asynchronous channels. It has long been known that CSP is capable of modeling shared variables or asynchronous channels as processes. However, the dedicated language constructs offer great usability and may make the verification more efficient.
The third group is a set of event annotations. It is known that process algebra like CSP or CCS specifies safety only. The event annotations offer a flexible way of modeling fairness using an event based compositional language.
The last group is the language for stating assertions, which later may be automatically verified using the built-in verifiers.

The language syntax structures are listed as follows. The complete grammar rules and process laws can be found in Section 3.1.1.5 and Section 3.1.1.6 respectively.

3.1.1.1 Global Definitions

3.1.1.2 Process Definitions

3.1.1.3 Assertions